COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	goedel[f81,jmc]		Kreisel's essence of Goedel's theorem and applications
C00006 ENDMK
C⊗;
goedel[f81,jmc]		Kreisel's essence of Goedel's theorem and applications

From Kreisel's Goedel obituary

	"Let  S  be a class of (formulas defining) number-theoretic
predicates with one and two arguments, closed under identification of
variables and negation; thus if  F(n,m)  is in  S, so is  ¬F(n,n).
Then there is no (binary) predicate in  S  which enumerates all
(monadic) predicates in  S.  This means, as usual, that no formula
F(n,m)  in  S  has the property:

	[for each formula  G(m) of  S  there is a number  g'  such that

	∀m[F(g',m) ≡ G(m)].

a counter example is obtained by taking  ¬F(m,m)  for  G(m), and putting
  m = g'."

The above is the essence of the proof of Goedel's first incompleteness
theorem.

	The following is a purely logical version of the theorem that was
on the Stanford Computer Science Comprehensive Examination in February 1982.

	"Let G(x,y) be a predicate defined on a domain D.  A unary predicate
F(x) is called representable by G if there is an element  a  of  D  such that
∀x.F(x) ≡ G(a,x).  Prove that there is always a non-representable predicate."

Most students solved the problem by setting  F(x) ≡ ¬G(x,x).  One used
a cardinality argument to make the proof.

	Perhaps, the theorem can be used to prove the undecidability of
totality of LISP functions as follows: (i) In the above, replace
"number-theoretic" by
"LISP-theoretic".  (ii) Let  S  be the class of all total LISP functions
of one and two arguments.  (iii) The  F(n,m) shown not to exist would
enumerate all total one argument LISP predicates.  Hmm, this isn't
obviously what we want.  Oh yes, it gives us what we want.  Suppose we
had a total LISP function  total(e)  that determined whether a LISP
function were total.  Then the function   F(n,m)  defined by

	F(n,m) ← if total(n) then eval(<n,<quote,m>>,nil) else ATOM

would enumerate all total LISP predicates in Kreisel's sense.

	This proves there is no test for totality.  A bit more must
be said to show that termination is undecidable in the individual
case.  Suppose the predicate 

	terminates(fn,arg),

which is true iff the application of the function  fn  to the list
args  of arguments terminates, were a LISP function.  Then

	P(n,m) = if terminates(n,m) then eval(<n,<quote,m>>,nil) else nil

	¬P(n,n) = if terminates(n,n) then ¬eval(<,<quote,n>>,nil) else true

		= P(a,n)